es:ES, b:, x:Id, e:{e:E| @loc(e)(x:)} .
((x when e) = b)
 ((x initially@loc(e)  = (b)  )  (e':E. (e' loc e  & (x when e') = (b)  )))
 (e':E
 (((e' <loc e)
 (& (x when e') = (b)  
 (& (x after e') = b
 (& e''(e',e].(x when e'') = b
 (& e''[e',e).(x after e'') = b)) 

latex

Definitions

P  Q, P  Q, {T}, SQType(T), ff, tt, if b then t else f fi , x. t(x), A c B, , t  T, lastchange(x;e), (e <loc e'), e loc e' , P & Q, x:A. B(x), P  Q, P  Q, x:A. B(x), A, False, @e(xv), Unit, , x(s), @i(x:T),

Lemmas

es-le wf, has-changed, init-not-changed, last-change-after-property, last-change wf, equal-bnot, bool sq, last-change-property, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, bnot wf, changed wf, event system wf, Id wf, es-dtype wf, es-E wf, es-le-loc, es-locl wf, es-initially wf, alle-between1 wf, es-locl-iff, es-loc-pred, es-first wf, assert wf, not wf, alle-between3 wf, es-after wf, es-vartype wf, es-when wf, es-causl wf, es-loc wf, bool-deq wf, bool wf, es-lc wf